p:FinProbSpace, a:, f:(), X:(n:RandomVariable(p;f(n))).
rv-iid(p;n.f(n);n.X(n))  rv-iid(p;n.f(n);n.X(n) + a) 

latex

Definitions

t  T, RandomVariable(p;n), f(a), x(s), n+m, P  Q, False, A, P & Q, A  B, i  j < k, , {x:A| B(x)} , , {i..j}, x:AB(x), x:A. B(x), rv-const(a), #$n, FinProbSpace, x,y:A//B(x;y), , rv-disjoint(p;n;X;Y), a < b, rv-identically-distributed(p;n.f(n);i.X(i)), rv-iid(p;n.f(n);i.X(i)), x:A  B(x), s = t, A c B, x.A(x), x. t(x), Type, r * s, P  Q, P  Q, (x.F(x)) o X, E(n;F), <a, b>, Void, x:A.B(x), Top, type List, S  T, , A  B, , EquivRel(T;x,y.E(x;y)), tt, qeq(r;s), , x,y. t(x;y), ||as||, True, T, left + right, P  Q, Dec(P), {T}, SQType(T), s ~ t

Lemmas

decidable int equal, subtype rel function, squash wf, true wf, int seg properties, subtype rel weakening, ext-eq weakening, int seg wf, length wf nat, quotient wf, bool wf, qeq wf2, btrue wf, b-union wf, int nzero wf, top wf, expectation-rv-const, qmul wf, rv-iid wf, random-variable wf, rationals wf, finite-prob-space wf, rv-iid-add, nat wf, le wf, rv-disjoint-symmetry, rv-disjoint-const, rv-const wf